-- David Siegel, Jonathan Coveney, HW #8

module Main where

import Char
import System.IO
import System.Exit
import qualified List
import System.Environment

import Term
import Routine
import qualified Set
import qualified Logic
import qualified Parsing
import qualified TermParser as Parser
import qualified TermLexer
import qualified Testing

main :: IO ()
main =
    do argv <- getArgs
       if argv == []
         then do putStrLn "USAGE: prove <knowledge-base>"
                 exitFailure
         else return ()

       kb <- loadKB (head argv)
       if Logic.satisfiable kb
           -- Run the main event loop.
           then queryKB kb
           else do putStrLn "Your knowledgebase is unsatisfiable."
                   exitFailure

-- A list of interactive routines the user can perform in the main
-- event loop. Names, descriptions, usage syntax, and function pointers
-- are stored in one location so it's easy to add new routines. Also,
-- we generate our help information from this list.
routines =
    [Simple "about"
            "Displays information about the program"
            about,
     Simple "help"
            "Displays a list of commands"
            usage,
     Simple "ls"
            "Lists sentences in the knoweldgebase"
            printKB,

     -- Complex Routines:
     Complex "prove"
             "Attempts to prove a sentence from the knowledgebase"  
             "prove SENTENCE"
             prove,
     Complex "sat"
             "Attempts to satisfy a sentence with the knowledgebase"
             "sat SENTENCE"
             sat,
     Complex "add"
             "Adds a sentence to the knowledgebase"                 
             "add SENTENCE"
             addToKB,
     Complex "rm"
             "Removes a sentence from the knowledgebase"            
             "rm SENTENCE-NUMBER"
             removeFromKB
    ]

------------------------------------------------------------
-- Private method declarations
------------------------------------------------------------

-- Runs testing code for all modules.
test :: IO ()

-- List of routines the user can perform.
routines :: [Routine]

-- Try to parse input as Term. If parse fails, return to main event loop.
tryParse :: RoutineF

-- Given a FilePath, loads the file, attempting to parse each line as a sentence
-- in proppositional logic.  Reports errors with line numbers.
loadKB :: FilePath -> IO KnowledgeBase

-- Main event loop. Prompts user for sentences to satisfy until the user presses
-- RETURN.
queryKB :: KnowledgeBase -> IO ()

-- Add a sentence to the knowledge base if the knowledgebase will not become
-- unsatisfiable as a result.
addToKB :: RoutineF

-- Remove a sentence (referenced by number) from the knowledgebase.
removeFromKB :: RoutineF

-- Print the knowledge base. Sentences are numbered for use with interactive
-- commands.
printKB :: RoutineF

-- Try to satisfy knowledgebase + sentence.
sat :: RoutineF

-- Try to prove a sentence from a knowledgebase.
prove :: RoutineF

-- Prints usage informaiton.
usage :: RoutineF

-- Prints information about the program.
about :: RoutineF

-- Given a path to a file, returns its contents as an array of strings.
fileToStrings :: FilePath -> IO [String]

-- Convert a string to a CNF Term.
stringToCNF :: String -> Term

-- Convert a string to a CNF Term string.
stringToCNFString :: String -> String

------------------------------------------------------------
-- Private method definitions
------------------------------------------------------------

queryKB kb =
    do  putStr "> "; hFlush stdout
        s <- getLine
        case words s of
          (r:rest) ->
              case lookupRoutineF r routines of
                  Just f  -> f (unwords rest) kb
                  Nothing ->
                    putStrLn "Unrecognized command. Type 'help' for help."
          -- If user enters nothing, exit.
          []       -> exitWith ExitSuccess
        -- Repeat
        queryKB kb

usage _ _ = do putStrLn "    ======== USAGE INFORMATION ========="
               mapM_ (putStrLn . show) routines
               putStrLn "Press RETURN to exit."

addToKB s kb =
    let t = Parser.justStringToTerm s in
    do tryParse s kb
       if Logic.satisfiable (t:kb)
         then queryKB (t:kb)
         else putStrLn "New knowledgebase is not satisfiable. Add failed."

removeFromKB line kb =
    case read line of
       (-1)     -> putStrLn "Bad line number."
       lineno   -> aux lineno
    where aux n
            | n > length kb = putStrLn "Line number is too large."
            | n < 1         = putStrLn "Line number is too small."
            | otherwise     = queryKB (remove n kb)
          -- Removes an element from a list.
          remove i xs = take (i-1) xs ++ drop i xs

printKB s kb = mapM_ p (zip [1..] kb)
               where p (line, term) =
                      putStrLn $ "  " ++ show line ++ ": " ++ show term 

sat s kb = do tryParse s kb
              case satisfyWith s of
                 Nothing -> putStrLn "No satisfying assignment."
                 Just ta -> putStrLn $ "Satisfied with assignment:\n"
                                         ++ showTa ta
              where satisfyWith s =
                      Logic.satisfy (Parser.justStringToTerm s : kb)

prove s kb = do tryParse s kb
                if proveWith s
                  then putStrLn "Knowledgebase proves the sentence." 
                  else putStrLn "Sentence does not follow from knowledgebase."
             where proveWith s = not $ Logic.satisfiable kb'
                   negTerm     = Not $ Parser.justStringToTerm s
                   kb'         = negTerm : kb

about _ _ = mapM_ putStrLn
      [" _   _ ____  _    _  _______",
       "| | | |  __|/ \\  / \\|__   __|",
       "| |_| | |_ |   \\/   |  | |",
       "|  _  |  _||  \\__/  |  | |",
       "| | | | |__|  |  |  |__| |__",
       "|_| |_|____|__|  |__|_______|\n",
       " \\*- THE ALL AMERICAN -*\\",
       "  \\*-   UNION MADE     -*\\",
       "   \\*- APPLE PIE EATING -*\\",
       "Propositional Logic Engine",
       "Just like mama used to make\n",
       "Completely free for distribution under the",
       "MIT LICENSE <== Penn didn't have a license :(\n",
       "Written for Benajmin Pierce",
       "(Who IRC assures us is a badass)\n",
       "   Written by",
       " > David Siegel",
       " > Jonathan Coveney"]

tryParse s kb =
    case Parser.stringToTerm s of
        Nothing -> do putStrLn "Malformed sentence."
                      queryKB kb
        _       -> return ()

loadKB file =
    do  putStrLn $ "Loading knowledge base from file \"" ++ file ++ "\"..."
        lines <- fileToStrings file
        let kb = map Parser.stringToTerm lines in
            -- If some sentence cannot be parsed, report the error.
            -- Otherwise, return the KnowledgeBase of parsed sentences.
            case List.elemIndex Nothing kb of
                Nothing   -> return $ map (\(Just t) -> t) kb
                Just line -> error $ "\"" ++ (lines !! line) ++
                                     "\" is a malformed sentence (line " ++
                                     show (line + 1) ++ ")."

fileToStrings path = do contents <- readFile path
                        return (lines contents)

stringToCNF = Logic.toCNF . Parser.justStringToTerm

stringToCNFString = show . stringToCNF

------------------------------------------------------------
-- Testing
------------------------------------------------------------

test = do Logic.test
          Parsing.test
          TermLexer.test
          Parser.test
          Set.test
